discrete\_struct\{i:l\}($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it sort}$:($A$$\rightarrow$Type\{i\}) $\times$ ($a$:$A$$\rightarrow$EqDecider(${\it sort}$($a$)))